\chapter{Podstawy teoretyczne} \label{chap:podstawy-teoretyczne}
Rozdział przedstawia podstawy teoretyczne potrzebne do
przejścia od ``ręcznego'' sprawdzania dowodów matematycznych do komputerowego (od
(\ref{sec:matematyka-klasyczna})
%(\ref{sec:matematyka-konstruktywistyczna}),
%(\ref{sec:pml}),
do (\ref{sec:kompilatory})), następnie przedstawia podstawy algebry (\ref{sec:podstawy-algebry}) oraz język programowania (\ref{sec:podstawy-agdy}) używane w rozdziale \ref{chap:wykonanie}.
\input{podstawy/przyklad.tex}
\input{podstawy/klasyczna.tex}
\input{podstawy/konstruktywistyczna.tex}
\input{podstawy/pml.tex}
\input{podstawy/kompilator.tex}
\input{podstawy/algebra.tex}
\input{podstawy/agda.tex}
